Skip to content

Conversation

@datokrat
Copy link
Collaborator

@datokrat datokrat commented Sep 3, 2025

This PR solves problem 106 twice -- (1) using a 1:1 translation of the Python reference implementation and (2) a DP-based solution of linear runtime. The verification is carried out using MPL.

It also adds the experimental.module = true option to the Lake file: I think it would be good to start using the module system here, too. I already noticed one library defect this way (see the comment on the imports).

@datokrat datokrat mentioned this pull request Sep 3, 2025
@datokrat datokrat marked this pull request as ready for review September 3, 2025 17:43
@datokrat datokrat marked this pull request as draft September 5, 2025 11:16
@datokrat datokrat marked this pull request as ready for review September 5, 2025 12:15
@datokrat datokrat merged commit 955976e into leanprover:master Jan 21, 2026
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants